(set-option :produce-models true)
(set-logic ALL)
(declare-fun s0 () String)
(declare-fun s1 () String)
(define-fun s2 () Bool (str.suffixof s0 s1))
(define-fun s3 () Bool (not s2))
(define-fun s4 () Int (str.len s1))
(define-fun s5 () Int (str.len s0))
(define-fun s6 () Int (- s4 s5))
(define-fun s7 () String (str.substr s1 s6 s5))
(define-fun s8 () Bool (= s0 s7))
(define-fun s9 () Bool (or s3 s8))
(assert (not s9))
(check-sat)
